when P, R1 => R2 == x, y:T. P(x)  (x R1 y)  (x R2 y) 

latex

---

clarification:

cond_rel_implies(T;P;R1;R2) == x:T, y:T. P(x)  (x R1 y)  (x R2 y) 

latex

Definitions	x:A. B(x), P  Q, x f y
FDL editor aliases	cond_rel_implies